∂03-FEB-75  0242		VCG,DCL
 Next Prover jam session is Friday Feb 7th at 11.30 in JRA's office.
 JFS continues with the analysis of what DAP has to offer in the
 way of new stategies.
 COMING TOPICS: Design of the useer strategy language--JFS
                Adding Evaluation to the prover.
                Automatic programming by prover and Answeer Extraction.
␈ CC: jra;jfs;jjm;dcl

∂03-FEB-75  0238		VCG,DCL
 The next Theorem Proving Seminar will be on Monday Feb.10th.
 at 4.15 in the AI Lab conference room (as usual). We had
 to postpone the Feb. 3rd meeting because of a clash with
 Mike Gordons theory of Programs meeting.
 On Feb 10th. John Allen will talk about how the prover really works.
␈ CC: JRA;JFS;JJM;GJP;GJD;DCL


∂30-JAN-75  1858		VCG,DCL
 Aha, I should have remembered that! It may not be the BEST thing
 to do, but why do you say it's the "wrong" thing to do?
 The idea was that nonfluent goals were cheap to test, whereas
 fluent goals were much more expensive, so that if an AND fails
 for nonfluent reasons, that should be known first. Usually,
 nonfluents represent TYPES so that this is pretty much in line
 with the standard programming practice of checking argument
 types before initiating a procedure call.
 Anyway, it can be overidden by the advice system TRY-BEFORE
 (if it works of course!). So the reordering seems reasonable.

∂21-JAN-75  2027		VCG,DCL
 I'll give you Oppen's thesis tomorrow-may have to discuss it with him,
 in which case will introduce you. You should let dick kieburtz have a copy 
 of yur book. Meanwhile, prepare for coming brianstorm sessions: FRAMES,
 LECTURE, NSF PROPOSAL.


∂20-JAN-75  0258		VCG,DCL
 Let me know todays progress; I can try some things Monday night.
 We shall be giving some Demos Wednesday and Thursday.
 Apparently Carnegie Mellon is "very happy" with JRB and his
 latest applications to the Business world!
 Dont forget yyu owe me a lecture!!!


∂16-JAN-75  2202		VCG,DCL
 I might have to take back my previous msg.(not
 sure yet since system very slow) but with a little
 advice (bless old jacks soul) the new compiled version
 PFIB2 seems to be working. Its answer, if it finally
 does work will be PROC1 on [ap,jra].
 I really want to finish off this compiler calamity
 FAST. We may have a student to put on it.

∂16-JAN-75  2037		VCG,DCL
 I discovered a very interesting fact:
 See your new disk area [AP,JRA]:
 Take the old Fibonacci frame FFIB1 and compile it
 to get PFIB1. Try the goal (FIB X3,N): it fucks up.
 Take the old compiled version of the same frame,
 PFIB and try the same goal: it works.
 Conclusion?
 I shall be in phone contact with JRB tomorrow 3.15pm
 and we might ask him any questions that would help
 us then.


∂14-JAN-75  1951		P,JRA
 FDIJK3[APG,DCL] and PDIJK3 almost worked. It looks to me
 as though the loop updating mechanism for computing the
 state after an ITERATIVE rule has been successful was
 running the loop body (which it is supposed to do only
 in the absence of an UPDATE statement in the rule--
 and got into the usual THUNASSIGNED). Since we have an 
 update statement somethings wrong. 


∂08-JAN-75  2340		VCG,DCL
 Ahha-we're getting close! We made that convention on
 variables in the loop having to be in the invariant 
 because of the way the "correct" loop constructing 
 algorithm should work. It can be gotten around by
 adding trivial statements like =(E1,E1) to the invariant.
 Remember ,you owe me a lecture on the correct loop-
 building algorithm.
 JFS has confirmed FRIDAY at 2.00p.m.
 I'm feeling happier about our having "a little disputational
 paper" replying to Dijkstra rather quickly now! 


∂02-JAN-75  1553		2,DCL
 Very interesting! Equality should be a NONFLUENT but in some JRB
 frames it was used as a FLUENT. I changed FDIJK so that equality
 was nonfluent, but it still stuck in compilation.Unfortunately,
 i'm not too sure how the algebraic simplification effects the 
 NONFLUENT property.
 I'm suggesting we consider the topic:"CAN PROGRAMMING LOOPS BE
 AUTOMATED".
 Notice in this system we are stuck with a simple view of the 
 world in which a variable is always distinct from its value.
 Let me know when you are well enough for our next meeting

∂29-DEC-74  1707		2,DCL
 I guess its time to set up a regular meeting between the two
 of us. 
 Tentative agenda: 1. WHILEASSEM, implementation and experiments.
 2.NSF proposal on programming lab.: projects and areas requiring
   additional staff.

∂13-DEC-74  1503		VCG,DCL
 There are a couple of extra loop frames around that could be
 used to test your new compr (but they may need a little
 editing):
 FTSL--the old Buchanan infix to prefix writer,
 FFIB1-- Fibonacci loop (easier).
 Both are on APG,DCL.
 the alternative is to write some new loop frames!